$\forall$${\it loc}$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it knd}$:Knd, $T$:Type, $x$:Id, $f$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$DeclaredType(${\it ds}$;$x$)).
\\[0ex]@${\it loc}$ effect ${\it knd}$(v:$T$)  $x$ := $f$ State(${\it ds}$) v  $\in$ Realizer